COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "book.pub[let,jmc]" source
C00006 00003	.ss First order logic with conditional terms and lambda-expressions.
C00019 00004	.ss Conditional terms.
C00025 00005	.ss Lambda-expressions.
C00027 00006	.ss Algebraic axioms for S-expressions and lists.
C00031 00007	.ss Axiom schemas of induction.
C00034 00008	.ss Proofs by structural induction.
C00037 00009	.ss First Order Theory of Partial Functions
C00041 ENDMK
C⊗;
.require "book.pub[let,jmc]" source;
.turn on "→"
.s		 PROVING LISP PROGRAMS CORRECT

	The theory of computation may be divided into
two parts.  The first is the general
theory of computability including topics like universal functions,
the existence of uncomputable functions, lambda calculus, call-by-name and
call-by-value, and the relation of conditional expression recursion
to other formalisms for describing computable functions.  The
second part, which we will discuss in this chapter emphasizes
techniques for proving particular facts about particular computable
functions.  We emphasize the use of the techniques
more than their mathematical background.

	We shall confine ourselves to proving %2extensional properties%1
of %2clean, pure%1 LISP programs.  An %2extensional property%1 is one that
depends only on the function computed by the program.  Thus it
includes the fact that two sort programs compute the same function
or that %2append%1 is associative but does not include the fact
that one sort program does %2n%52%1 comparisons and another %2n_log_n%1
comparisons.  %2Clean%1 LISP programs have no side effects (our
methods require the freedom to replace a subexpression by an equal
expression), and equality refers to the S-expressions and not to
the list structures.  %2Pure%1 LISP involves only recursive function
definitions and doesn't use assignment statements.
It wouldn't be difficult to give corresponding methods that would
be valid for non-functional programs, because this topic is well
developed.

	In spite of all these limitations, the techniques are useful and
point the way to further progress.

	The  necessary basic facts can be divided into several categories:
first order logic including conditional forms and first order
lambda-expressions, algebraic facts about lists and S-expressions,
facts about the inductive structure of lists and
S-expressions, and general facts about functions defined by
recursion.
.ss First order logic with conditional terms and lambda-expressions.

	The logic we shall use is called first order logic with equality,
but we will extend it by admitting conditional forms as terms and first
order lambda-expressions as function symbols.  These extensions do not
change the logical strength of the theory, because, as we shall see, every
sentence that includes conditional forms or first order lambdas can be
transformed into an equivalent sentence without them.  However, the
extensions are practically important, because they permit us to use
recursive definitions directly as formulas of the logic.

	Formulas of the logic are built from constants, variables
predicate symbols, and function symbols using function application,
conditional forms, boolean forms, lambda expressions, and quantifiers.

%3Constants%1: We will use S-expresssions as constants standing for
themselves and also lower case letters from the first part
of the alphabet to represent constants in other domains than
S-expressions.

%3Variables%1: We will use the letters %2u%1 thru %2z%1 with or
without subscripts as variables.  The variables %2u%1 and %2v%1
will usually stand for lists, while %2x%1 thru %2z%1 will stand
for S-expressions.  %2m%1 and %2n%1 are integer variables.

%3Function symbols%1: The letters %2f%1, %2g%1 and %2h%1 with or
without subscripts are used as function symbols.
The LISP function symbols %3a%1, %3d%1 and . (as an infix) are also
used as function symbols.
We suppose that each function symbol takes the same definite number of
arguments every time it is used.
Thus if the same letter is used with differing numbers of arguments,
it stands for different function symbols.
Thus we can use %2<x%41%2, ... ,x%4n%2>%1 to represent the list forming
functions, but we shall have to axiomatize it separately for each
length we actually use.
We will often use one argument functions symbols as prefixes, i.e.
without brackets, just as %3a%1 and %3d%1 have been used up to now.

%3Predicate symbols%1: The letters %2p%1, %2q%1 and %2r%1 with or
without subscripts are used as predicate symbols.  We will
also use the LISP predicate symbol %3at%1 as a constant predicate
symbol.  The equality symbol = is also used as an infix.
We suppose that each predicate symbol takes the same definite
number of arguments each time it is used.
Again a letter may be used with differing numbers of arguments to
represent different functions.
Infix and prefix notation will also be used where this is
customary.

	Next we define terms, sentences, function expressions
and predicate expressions inductively.  A term is
an expression whose value will be an object like an S-expression
or a number while a sentence has value T or F.
Terms are used in making sentences, and sentences occur in
terms so that the definitions are %2mutually recursive%1 where
this use of the word %2recursive%1 should be distinguished from
its use in recursive definitions of functions.
Function expressions are also involved in the mutual recursion.

%3Terms%1: Constants are terms, and variables are terms.  If
%2f%1 is a function expression taking %2n%1 arguments, and %2t%41%2,_..._,t%4n%2%1
are terms, then %2f[t%41%2,_..._,t%4n%2]%1 is a term.  If %2p%1 is
a sentence and %2t%41%2%1 and %2t%42%1 are terms, then
qif%2_p_qthen%2_t%41%2_qelse%2_t%42%1%1 is a term.  We soften the
notation by allowing infix symbols where this is customary.

%3Sentences%1:
If %2p%1 is a predicate expression taking %2n%1 arguments and
%2t%41%2,_..._,t%4n%2%1 are terms, then %2p[t%41%2,_..._,t%4n%2]%1 is
a sentence.  Equality is also used as an infixed predicate
symbol to form sentences, i.e. %2t%41%2_=_t%42%1%1 is a sentence.
If %2p%1 is a sentence, then %2¬p%1 is also a sentence.  If
%2p%1 and %2q%1 are sentences, then %2p∧q%1, %2p∨q%1, %2p⊃q%1,
and %2p≡q%1 are sentences.  If %2p%1, %2q%1 and %2r%1 are
sentences, then qif%2_p_qthen%2_q_qelse%2_r%1 is a sentence.
If %2x%41%2,_...,_x%4n%2%1 are variables, and %2p%1 is a term, then
%2∃x%41%2_..._x%4n%2:t%1 and %2∀x%41%2_..._x%4n%2:t%1 are sentences.

%3Function expressions%1: A function symbol is a function expression.
If %2x%41%2,_..._,x%4n%2%1 are variables and %2t%1 is a term, then
%2[λx%41%2,_..._,x%4n%2:t]%1 is a function expression.

%3Predicate expressions%1: A predicate symbol is a predicate expression.
If %2x%41%2,_..._,x%4n%2%1 are variables and %2p%1 is a sentence, then
%2[λx%41%2,_..._,x%4n%2:p]%1 is a predicate expression.

	An occurrence of a variable %2x%1 is called bound if
it is in an expression of one of the forms %2[λx%41%2_..._x%4n%2:t]%1,
%2[λx%41%2_..._x%4n%2:p]%1, %2[∀x%41%2_..._x%4n%2:p]%1 or %2[∃x%41%2_..._x%4n%2:p]%1
where %2x%1 is one
of the numbered %2x%1's.  If not bound an occurrence is called free.

	The %2semantics%1 of first order logic consists of the rules
that determine whether a sentence is true
or false.  However, the truth or falsity of a sentence is relative
to the interpretation assigned to the constants, the function and predicate
symbols and the free variables of the formula.  We proceed as follows:

	We begin by choosing a domain.  In most cases,
the domain will include the S-expressions, and any S-expression constants
appearing in the formula stand for themselves.  We will allow for the
possibility that other objects than S-expressions exist, and some constants
may designate them.  A special constant symbol qw is used for the value
of the function defined by a Lisp program in case the computation doesn't
terminate; its use requires a justification that will be given later.

	Each function or predicate symbol is assigned a
function or predicate on the domain.  We will normally assign to the
basic LISP function and predicate symbols the corresponding basic LISP
functions and predicates.  Each variable appearing free in a sentence is
also assigned an element of the domain.  All these assignments constitute
an interpretation, and the truth of a sentence is relative to the
interpretation.

	The truth of a sentence is determined from the values of its
constituents by evaluating successively larger subexpressions.  The
rules for handling functions and predicates, conditional expressions,
equality, and Boolean expressions are exactly the same as those we
have used in the previous chapters.  We need only explain quantifiers:

	%2∀x%41%2_..._x%4n%2:e%1 is assigned true if and only if %2e%1 is assigned
true for all assignments of elements of the domain to the %2x%1's.  If
%2e%1 has free variables that are not among the %2x%1's, then the
truth of the sentence depends on the values assigned to these remaining
free variables.  %2∃x%41%2_..._x%4n%2:e%1 is assigned true if and only if %2e%1
is assigned true for %2some%1 assignment of values in the domain to
the %2x%1's.  Free variables are handled just as before.

	%2λx%41%2_..._x%4n%2:u%1 is assigned a function or predicate according
to whether %2u%1 is a term or a sentence.  The value of
%2[λx%41%2_..._x%4n%2:u][t%41%2,...,t%4n%2]%1 is obtained by evaluating the 
%2t%1's and using these values as values of the %2x%1's in the
evaluation of %2u%1.  If %2u%1 has free variables in addition to the %2x%1's,
the function assigned will depend on them too.

	Those who are familiar with the lambda calculus should note
that λ is being used here in a very limited way.  Namely, the variables
in a lambda-expression take only elements of the domain as values,
whereas the essence of the lambda calculus is that they take arbitrary
functions as values.  We may call these restricted lambda expressions
%2first order lambdas%1.
.ss Conditional terms.

	All the properties we shall use of conditional terms follow
from the relation

	%2[p ⊃ [qif p qthen a qelse b] = a] ∧ [¬p ⊃ [qif p qthen a qelse b] = b]%1.

	It is worthwhile to list separately some properties
of conditional terms.

	First we have the obvious

	%2qif T qthen a qelse b = a%1

and

	%2qif F qthen a qelse b = b%1.

	Next we have a %2distributive law%1 for functions applied
to conditional terms, namely

	%2f[qif p qthen a qelse b] = qif p qthen f[a] qelse f[b]%1.

This applies to predicates as well as functions and can also be used
when one of the arguments of a function of several arguments is a
conditional term.  It also applies when one of the terms of
a conditional term is itself a conditional term.

Thus

	%2qif [qif p qthen q qelse r] qthen a qelse b =
qif p qthen [qif q qthen a qelse b] qelse [qif r
qthen a qelse b]%1

and

	%2qif p qthen [qif q qthen a qelse b] qelse c =
qif q qthen [qif p qthen a qelse c] qelse [qif p
qthen b qelse c]%1.

	When the expressions following qthen and qelse are
sentences, then the conditional term can be replaced by a sentence
according to

	%2[qif p qthen q qelse r] ≡ [p ∧ q] ∨ [¬p ∧ r]%1.

These two rules permit eliminating conditional terms from sentences
by first using distributivity to move the conditionals
to the outside of any functions and then replacing the conditional
term by a Boolean expression.

	Note that the elimination of conditional terms may increase
the size of a sentence, because %2p%1 occurs twice in the right
hand side of the above equivalence.  In the most unfavorable case,
%2p%1 is dominates the size of the expression so that writing it
twice almost doubles the size of the expression.

	Suppose that %2a%1 and %2b%1 in
%2qif_p_qthen_a_qelse_b%1
are expressions that may contain the sentence %2p%1.  Occurrences
of %2p%1 in %2a%1 can be replaced by T, and occurrences of %2p%1
in %2b%1 can be replaced by F.  This follows from the fact that
%2a%1 is only evaluated if %2p%1 is true and %2b%1 is evaluated only
if %2p%1 is false.

	This leads to a strengthened form of the law of replacement
of equals by equals.  The ordinary form of the law says that if
we have %2e_=_e'%1, then we can replace any occurrence of %2e%1
in an expression by an occurrence of %2e'%1.  However, if we want
to replace %2e%1 by %2e'%1 within %2a%1 within
qif%2_p_qthen%2_a_qelse%2_b%1,
then we need only prove %2p_⊃_e_=e'%1, and to make the replacement
within %2b%1 we need only prove %2¬p_⊃_e_=_e'%1.

	More facts about conditional terms are given in (McCarthy 1963a)
including a discussion of canonical forms that parallels the canonical
forms of Boolean terms.  Any question of equivalence of conditional
terms is decidable by truth tables analogously to the decidability of
propositional sentences.
.ss Lambda-expressions.

	The only rule required for handling lambda-expressions
in first order logic is called %2lambda-conversion%1, essentially

	%2[λx:e][a] =%1 <the result of substituting %2e%1 for %2x%1 in %2a%1>.

As examples of this rule, we have

	%2[λx:qa x . y][u . v] = [qa [u . v]] . y%1.

However, a complication requires modifying the rule.  Namely,
we can't substitute for a variable ⊗x an expression ⊗e that has a free variable
⊗y into a context in which ⊗y is bound.  Thus it would be
wrong to substitute %2y_+_z%1 for %2x%1 in %2∀y:[x_+_y_=_z]%1 or into
the term %2[λy:x_+_y][u_+_v]%1.  Before doing the substitution, the
variable %2y%1 would have to be replaced in all its bound occurrences by
a fresh variable.

	Lambda-expressions can always be eliminated from sentences and
terms by lambda-conversion, but the expression may increase greatly
in length if a lengthy term replaces a variable that occurs more than
once in %2e%1.  It is easy to make an expression of length %2n%1 whose
length is increased to 2%5n%1 by converting its %2n%1 nested lambda-expressions.

.ss Algebraic axioms for S-expressions and lists.

	The algebraic facts about S-expressions are expressed
by the following sentences of first order logic:

	%2∀x.(issexp x ⊃ qat x ∨ (issexp qa x ∧ issexp qd x
∧ x = (qa x . qd x)))%1

and

	%2∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬qat(x.y)
∧ x = qa(x.y) ∧ y = qd(x.y))%1.

Here %2issexp e%1 asserts that the object %2e%1 is an S-expression
so that the sentences used in proving a particular program correct
can involve other kinds of entities as well.
If we can assume that all objects are S-expressions or can declare certain
variables as ranging only over S-expressions, we can simplify the axioms
to

	%2∀x.[qat x ∨ x = [qa x . qd x]]%1

and

	%2∀x y.[¬qat[x.y] ∧ x = qa[x.y] ∧ y = qd[x.y]]%1.


	The algebraic facts about lists are expressed by the following
sentences of first order logic:

	%2∀x. islist x ⊃ x = qNIL ∨ islist qd x%1,

	%2∀x y. islist y ⊃ islist[x . y]%1,

	%2∀x y. islist y ⊃ qa[x . y] = x ∧ qd[x.y] = y%1.

We can rarely assume that everything is a list, because the
lists usually contain atoms which are not themselves lists.

	These axioms are analogous to the algebraic part of Peano's
axioms for the non-negative integers.  The analogy can be made clear
if we write Peano's axioms using %2n'%1 for the successor of %2n%1
and %2n%5-%1 for the predecessor of %2n%1.  Peano's algebraic axioms
then become

	%2∀n: n' ≠ 0%1,

	%2∀n: (n')%5-%2 = n%1,

and

	%2∀n: n ≠ 0 ⊃ (n%5-%2)' = n%1.

Integers specialize  lists if we identify 0 with qNIL and assume that
there is only one object (say 1) that can serve as a list element.
Then %2n'_=_cons[1,n]%1, and %2n%5-%2_=_qd n%1.

	Clearly S-expressions and lists satisfy the axioms given for them,
but unfortunately these algebraic axioms are insufficient to
characterize them.  For example, consider a domain of one element
%2a%1 satisfying

	%2qa a = qd a = a . a = a%1.

It satisfies the algebraic axioms for S-expressions.  We can exclude
it by an axiom %2∀x.(qa x ≠ x)%1, but this won't exclude other
circular list structures that eventually return to the same element
by some %3a-d%1 chain.  Actually we want to exclude all infinite
chains, because most LISP programs won't terminate unless every
%3a-d%1 chain eventually terminates in an atom.  This cannot be
done by any finite set of axioms.

.ss Axiom schemas of induction.

	
	In order to exclude circular and infinite list structures we need
axiom schemas of induction analogous to Peano's for the integers.  Peano's
induction schema is ordinarily written

	%2P(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)%1.

Here %2P(n)%1 is an arbitrary predicate of integers, and we get particular
instances of the schema by substituting particular predicates.
It is called an axiom schema rather than an axiom, because we consider
the schema, which is not properly a sentence of first order logic, as
standing for the infinite collection of axioms that arise from it by
substituting all possible predicates for %2P%1.
Peano's induction schema can also be written 

	%2∀n:(n = 0 ∨ P(n%5-%2) ⊃ P(n)) ⊃ ∀n:P(n)%1,

and the equivalence of the two forms is easily proved.

	The S-expression analog of this second form is

	%2∀x:[issexp x ⊃ [qat x ∨ P[qa x] ∧ P[qd x] ⊃ P[x]]] ⊃
∀x:[issexp x ⊃ P[x]]%1,

or, declaring the variable ⊗x to range over S-expressions,

	%2∀x:[qat x ∨ P[qa x] ∧ P[qd x] ⊃ P[x]] ⊃ ∀x:P[x]%1.

	The corresponding axiom schema for lists is

	%2∀u:[qn u ∨ P[qd u] ⊃ P[u]] ⊃ ∀u:P[u]%1.

	These schemas are called principles of %2structural induction%1,
since the induction is on the structure of the entities involved.

	Even the axiom schemas don't assure us that the only domain
satisfying the axioms is that of the integers or the S-expressions as
the case may be.  Any first order theory whose axioms
can be given effectively admits the so-called %2non-standard models%1.
However, it seems likely that the non-standard models of S-expressions,
like the non-standard models of integers, will agree with the standard
model for sentences of practical interest.
.ss Proofs by structural induction.

	Recall that the operation that appends two lists is defined by

!!si2:	%2u * v ← qif n u qthen v qelse qa u . [qd u * v]%1.

Assume that
%2u * v%1 is defined for all %2u%1 and %2v%1, i.e. the computation
described above terminates for all %2u%1 and %2v%1; we will
show how to prove it later.  Then we can replace ({[5] si2})
by the sentence

!!si1:	%2∀u v:[islist u ∧ islist v ⊃
[%2u * v = qif qn u qthen v qelse qa u . [qd u * v]]]%1.

Now suppose we would like to prove %2∀v:[qNIL * v = v]%1.  This is
quite trivial; we need only substitute qNIL for %2x%1 in ({[5] si1}),
getting

→%2qNIL * v ∂(15)_= qif n qNIL qthen v qelse a qNIL . [qd qNIL * v]

∂(15)_= v%1.

Next consider proving %2∀u:[u * qNIL = u]%1.  This cannot be done by
simple substitution, but it can be done as follows:  First substitute
%2λu:[u * qNIL = u]%1 for %2P%1 in the induction schema

	%2∀u:[islist u ⊃ [qn u ∨ P[qd u] ⊃ P[u]]] ⊃ ∀u:[islist u
⊃ P[u]]%1,

getting

	%2∀u:[islist u ⊃ [qn u ∨ [λu: u * qNIL = u][qd u]
⊃ %2λu:[u * qNIL = u][u]]] ⊃ ∀u:[islist u
⊃ %2λu:[u * qNIL = u][u]]%1.

Carrying out the indicated lambda conversions makes this

!!si3:	%2∀u:[islist u ⊃ [qn u ∨ qd u * qnil = qd u]
⊃ u * qnil = u] ⊃ ∀u:[islist u ⊃ u * qnil = u]%1.

	Next we must use the recursive definition of %2u*v%1.  There
are two cases according to whether qn %2u%1 or not.
In the first case, we substitute qnil for %2v%1 and get qnil*qnil_=_qnil,
and in the second case we use the hypothesis qd_u_*_qnil_=_qd_u and the
third algebraic axiom for lists to make the simplification

!!si4:	%2qa u . [qd u * qnil] = qa u . qd u = u.%1

Combining the cases gives the hypothesis of ({eq si3}) and hence
its conclusion, which is the statement to be proved.
.ss First Order Theory of Partial Functions

	In the previous section we proved facts about Lisp functions
starting from the assumption that their computation terminated for all
values of the arguments.  This enabled us to write the definition as a
sentence of first order logic.  However, when we write down a recursive
function definition we have no guarantee that it terminates for all
arguments.  Sometimes the problem is to prove that the computation
terminates, sometimes the problem is to prove that it doesn't, sometimes
we must establish that it terminates for arguments in a certain set and
not otherwise, and sometimes we want to establish that two function
definitions are equivalent without determining for what values either
terminates.

	Even though a recursively defined function is not known to
terminate, it is still possible to characterize in first order logic.
This is done as follows:

	Consider the domain ⊗SE of S-expressions to be imbedded in
a larger domain.  For concreteness we may suppose that this domain
has only one element %Aw%1 besides the S-expressions that we will
take as the value of a function whenever its computation fails to
terminate.  We may further assume that the basic Lisp functions
take %Aw%1 as value whenever an argument has value %Aw%1.  However,
neither assumption will ever be used in a proof, so their need be
no axioms expressing them.

	Recursive definitions give rise to logical sentences just as before
so that ⊗append is described by

!!b1:	%2∀u v.[u * v = qif qn u qthen v qelse qa u . [qd u * v]]%1,

but now it is not assumed that %2u_*_v%1 is a list; it
might be %Aw%1 or any other element of the %2outer domain%1.  However,
we can prove that %2u_*_v%1 is a list for all lists ⊗u and ⊗v by
induction as follows:

	We take

!!b2:	%2P(u) = islist[u * v]%1

in the axioms schema of list induction getting

!!b3:	%2islist[qnil * v] ∧ ∀u.[¬qn u ∧ islist[qd u * v] ⊃ islist[u * v]]⊃ ∀u.islist[u * v]%1.

Now the premisses of ({eq b3}) are easily proved from ({eq b1}) and
the fact that if ⊗u is a list, so is %2x_._u%1.  As we shall see,
the resulting proof that the computation of %2u_*_v%1 is a list
can be taken as also proving that the computation terminates.